Library cross_conjugate
Require Export PointsType.
Require Import incidence.
Require Import TrianglesDefs.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition cross_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
cTriple (u/(- p×v×w + q×w×u + r×u×v)) (v/(p×v×w - q×w×u + r×u×v)) (w/(p×v×w + q×w×u - r×u×v))
end.
Require Import incidence.
Require Import TrianglesDefs.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition cross_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
cTriple (u/(- p×v×w + q×w×u + r×u×v)) (v/(p×v×w - q×w×u + r×u×v)) (w/(p×v×w + q×w×u - r×u×v))
end.
The P-cross conjugate of U, is the perspector of ABC and the cevian triangle P in the cevian triangle of U.
Lemma cross_conjugate_property :
∀ P U,
match P, U with
cTriple X Y Z, cTriple X1 Y1 Z1 ⇒
- X × Y1 × Z1 + Y × Z1 × X1 + Z × X1 × Y1 ≠ 0 →
X × Y1 × Z1 - Y × Z1 × X1 + Z × X1 × Y1 ≠ 0 →
X × Y1 × Z1 + Y × Z1 × X1 - Z × X1 × Y1 ≠ 0 →
match cevian_triangle U with
(A',B',C') ⇒
is_perspector (cross_conjugate P U) (pointA,pointB,pointC) (cevian_triangle_gen P A' B' C')
end
end.
Proof.
intros.
destruct P.
destruct U.
simpl.
unfold is_perspector, col.
simpl.
repeat split;
field;
intuition.
Qed.
End Triangle.